l:IdLnk, da:fpf(Knd; k.Type). es-dt(l; da)  fpf(Id; tg.Type) 

latex

Definitions	Knd, t  T, isl(x), , if b then t else f fi , x:A. B(x), b, rcv(l,tg), P  Q, , Unit, tag(k), lnk(k), eq_lnk(a; b), isrcv(k), x. t(x), compose-fpf(a; b; f), fpf(A; a.B(a)), es-dt(l; da), IdLnk, Id, ff, A, b, prop{i:l}, P  Q, P  Q, False, True
Lemmas	not functionality wrt iff, assert-eq-lnk, true wf, false wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, bfalse wf, fpf wf, IdLnk wf, compose-fpf wf, isrcv wf, ifthenelse wf, eq lnk wf, lnk wf, tagof wf, unit wf, it wf, rcv wf, Id wf, assert wf, Knd wf